Inference at * 2 0 1 
Iof proof for Lemma multiply nat wf:



1. i : 
2. j : 
3. j  0 
  0  (i * j) 

latex

 by (\p.IntInd (get_int_arg `hn` p) p) 

latex

 1: .....downcase..... NILNIL

 1: 3. j < 0
 1: 4. ((j+1)  0 )  (0  (i * (j+1)))
 1:   (j  0 )  (0  (i * j))
 2: .....basecase..... NILNIL

 2: 1. i : 
 2:   (0  0 )  (0  (i * 0))
 3: .....upcase..... NILNIL

 3: 3. 0 < j
 3: 4. ((j - 1)  0 )  (0  (i * (j - 1)))
 3:   (j  0 )  (0  (i * j))
 .

Definitions

n - m, n+m, a < b, n * m, A  B, #$n, i  j , , , x:AB(x), P  Q